Reset Initial.
(*************************************************************************)
(** simply-typed Scalina  in Coq. *)
(*************************************************************************)

(** Based on:
    An interactive tutorial on developing programming language
    metatheory.  This file uses the simply-typed lambda calculus
    (STLC) to demonstrate the locally nameless representation of
    lambda terms and cofinite quantification in judgments.

    This tutorial concentrates on "how" to formalize STLC; for more
    details about "why" we use this style of development see:
    "Engineering Formal Metatheory", Aydemir, Charguéraud, Pierce,
    Pollack, Weirich. POPL 2008.

    Tutorial authors: Brian Aydemir and Stephanie Weirich, with help
    from Aaron Bohannon, Nate Foster, Benjamin Pierce, Jeffrey
    Vaughan, Dimitrios Vytiniotis, and Steve Zdancewic.  Adapted from
    code by Arthur Charguéraud.
*)

(*************************************************************************)

(* First, we import a number of definition from the Metatheory
   library (see Metatheory.v). The following command makes those
   definitions available in the rest of this file. This command
   will only succeed if you have already run "make" in the tutorial
   directory to compile the Metatheory library.
*)
Require Import Metatheory.

(*************************************************************************)
(** * Syntax of Simply Typed Scalina *)
(*************************************************************************)

(** We use a locally nameless representation, where bound variables are 
    represented as natural numbers (de Bruijn indices) and free variables
    are represented as [atom]s.  The type [atom], defined in the [Atom] library,
    represents names: equality is decidable on atoms (eq_atom_dec), 
    and it is possible to generate an atom fresh for any given 
    finite set of atoms (atom_fresh_for_set).
*)

(*
Inductive level : Set := terms | types | kinds.
Inductive lab   : level -> Set
Inductive classified : level -> Set
  | cls_tm : option tm -> tp -> classified terms
  | cls_tp : option tp -> kd -> classified types.
Inductive mem (L: level)  :  Set = 
  | m : lab L -> classified L -> mem L.
*)

Inductive lab : Set :=
  | ltm  : nat -> lab.  (* term label *)
(*  | ltp  : nat -> lab.  (* type label *) *)

Inductive tp : Set :=
  | tp_struct : option tp -> list mem  -> tp (* self type, list of members *)

(* due to recursive structure, using a set to hold the members is too 
complicated -- this is more faithful to distinction between syntax and 
well-formedness anyway*)

with mem : Set :=
  | mtm : lab -> tp -> option tm -> mem

with tm : Set :=
  | bvar : nat  -> tm    (* bound variables *)
  | fvar : atom -> tm   (* free  variables *)
  | sel  : tm -> lab  -> tm
  | new  : tp  -> tm.

Coercion bvar : nat >-> tm.
Coercion fvar : atom >-> tm.

Fixpoint lab_getIdx (l: lab) {struct l} : nat :=
  match l with
  | ltm n => n
(*  | ltp n => n*)
  end.

Fixpoint mem_getLabel (m: mem) {struct m} : lab :=
  match m with
  | mtm l _ _ => l
  end.

(** We declare the constructors for indices and variables to be
    coercions. That way, if Coq sees a [nat] where it expects an
    [exp], it will implicitly insert an application of [bvar]; and
    similarly for [atom]s.
*)


(** There are two important advantages of the locally nameless
    representation:
     - Alpha-equivalent terms have a unique representation, 
       we're always working up to alpha-equivalence.
     - Operations such as free variable substitution and free
       variable calculation have simple recursive definitions
      (and therefore are simple to reason about).

    Weighed against these advantages are two drawbacks:
     - The [exp] datatype admits terms, such as [abs 3], where
       indices are unbound. 
       A term is called "locally closed" when it contains 
       no unbound indices. 
     - We must define *both* bound variable & free variable 
       substitution and reason about how these operations 
       interact with eachother.
    
*)


(*************************************************************************)
(** * Substitution *)
(*************************************************************************)

(** Substitution replaces a free variable with a term.  The definition
    below is simple for two reasons:
      - Because bound variables are represented using indices, there
        is no need to worry about variable capture.
      - We assume that the term being substituted in is locally
        closed.  Thus, there is no need to shift indices when
        passing under a binder.
*)

Fixpoint subst_tm (z : atom) (u : tm) (e : tm) {struct e} : tm :=
  match e with
    | bvar i => bvar i
    | fvar x => if x == z then u else (fvar x)
    | sel e1 l => sel (subst_tm z u e1) l
    | new T => new (subst_tp z u T)
  end

with subst_tp (z : atom) (u : tm) (e : tp) {struct e} : tp :=
  match e with
    | tp_struct self mems => tp_struct (option_map (subst_tp z u) self) (List.map (subst_mem z u) mems)
  end

with subst_mem (z : atom) (u : tm) (e : mem) {struct e} : mem :=
  match e with
    | mtm l T rhs => mtm l (subst_tp z u T)  (option_map (subst_tm z u) rhs)
  end.

(** The Fixpoint keyword defines a Coq function. As all functions in 
    Coq must be total, the annotation [{struct e}] indicates the termination 
    metric---all recursive calls in this definition are made to
    arguments that are structurally smaller than [e].
*)

(* Note also that subst uses the notation [x == z] for
   decidable atom equality. (This notation is defined in
   [Metatheory].)
*)


(*Fixpoint option_getOrElse (A: Set) (alt: A) (o: option A)  : A :=
  match o with
    | None => alt
    | (Some x) => x
  end.

Implicit Arguments option_getOrElse [A].
*)

Definition option_fold (A:Set) (B:Type) (f:A->B) (b:B) o :=
  match o with
  | None => b
  | Some x => f x
  end.

Implicit Arguments option_fold [A B].


(*************************************************************************)
(** * Free variables *)
(*************************************************************************)

(** The function [fv], defined below, calculates the set of free
    variables in an expression.  Because we are using locally nameless
    representation, where bound variables are represented as indices,
    any name we see is a free variable of a term.  In particular, this
    makes the [abs] case simple.
*)

Require Import FSets.


Fixpoint fv_tm (e : tm) {struct e} : atoms :=
  match e with
    | bvar i => {}
    | fvar x => singleton x
    | sel e1 l => fv_tm e1
    | new T => fv_tp T
  end

with fv_tp (e : tp) {struct e} : atoms :=
  match e with
    | tp_struct self mems => AtomSet.F.union (option_fold fv_tp {} self) 
         (fold_left (fun (ats: atoms) (m :  mem) => AtomSet.F.union ats (fv_mem m)) mems {})
  end

with fv_mem (e : mem) {struct e} : atoms :=
  match e with
    | mtm l T rhs => AtomSet.F.union (fv_tp T)  (option_fold fv_tm {} rhs)
  end.

(** We define a notation for free variable substitution that mimics
    standard mathematical notation. *)

Notation "[ z ~> u ] e" := (subst_tm z u e) (at level 68).
Notation "[ z ~tp> u ] t" := (subst_tp z u t) (at level 68).
Notation "[ z ~mem> u ] m" := (subst_mem z u m) (at level 68).


Fixpoint option_forAll (o: option Prop): Prop :=
  match o with
    | None => True 
    | (Some x) => x
  end.


(** weird that I couldn't find this in StdLib *)
Fixpoint list_forAll (l: list Prop): Prop :=
  match l with
    | (cons x xs) => x /\ (list_forAll xs)
    | nil => True
  end.

Lemma under_forAll_map: forall (A: Set) (xs: list A) (f g : A -> Prop),
  (forall x : A, f x -> g x) -> (list_forAll (List.map f xs)) -> (list_forAll (List.map g xs)).
  intros.
  induction xs; simpl in *; auto.
    inversion H0. split.
      apply (H a H1).
      apply (IHxs H2).
Qed.    
    
(** TODO: use under_forAll_map **)
Lemma list_forAll_MP: forall (A : Set) (l : list A)  (P: A -> Prop) (Q: A -> Prop),
    list_forAll (List.map (fun x: A => P x -> Q x) l) -> list_forAll (List.map (fun x: A => P x) l) -> list_forAll (List.map (fun x: A => Q x) l).
Proof.
  intros A l P Q H.
  induction l. simpl. auto. simpl. induction H. split. apply H. destruct H1. assumption. destruct H1. apply (IHl H0 H2).
Qed.

Lemma list_forAll_eq_dist : forall (A : Set) (l : list A)  (f: A -> A),
  list_forAll (List.map (fun x : A => f x = x) l) -> List.map f l = l.
Proof.
  intros A l f H.
  induction l. 
    auto.
 
    simpl in *. 
      induction H. 
        rewrite H. f_equal. apply (IHl H0).
Qed.

Lemma list_forAll_eq_dist2 : forall (A : Set) (l : list A)  (f: A -> A) (g: A -> A),
  list_forAll (List.map (fun x : A => f x = g x) l) -> List.map f l = List.map g l.
Proof.
  intros A l f g H.
  induction l. 
    auto.
 
    simpl in *. 
      induction H. 
        rewrite H. f_equal. apply (IHl H0).
Qed.

Lemma list_forAll_eq_dist2_conv : forall (A : Set) (l : list A)  (f: A -> A) (g: A -> A),
  List.map f l = List.map g l -> list_forAll (List.map (fun x : A => f x = g x) l).
Proof.
  intros A l f g H.
  induction l; simpl in *. 
    auto.

  inversion H. split.  auto. apply IHl. assumption.
Qed.

(** TODO replace uses of list_map_compose and list_map_compose2 by map_map *) 
Lemma list_map_compose : forall (A : Set) (l : list A)  (f: A -> A) (g: A -> A),
  List.map f (List.map g l) = List.map (fun x => f(g(x))) l.
Proof.
  intros A l f g.
  induction l; simpl in *. 
    auto.
    f_equal. apply IHl.
Qed.

Lemma list_map_compose2 : forall (A : Set) (B : Set) (C : Type) (l : list A)  (f: B -> C) (g: A -> B),
  List.map f (List.map g l) = List.map (fun x => f(g(x))) l.
Proof.
  intros A B C l f g.
  induction l; simpl in *. 
    auto.
    f_equal. apply IHl.
Qed.

Functional Scheme fold_left_ind := Induction for fold_left Sort Prop.

Lemma foldUnionAssoc: forall A (f: A -> atoms) (xs: list A) (x: A),
 fold_left (fun (xs : atoms) (x : A) => xs `union` f x)
                xs ({} `union` f x) 
   =  fold_left (fun (xs : atoms) (x : A) => xs `union` f x)
                xs {} `union` f x.
Proof.
  intros. functional induction (fold_left  (fun (xs : atoms) (x : A) => xs `union` f x)
                xs {}).
  simpl. auto.
  simpl. replace ((a0 `union` f x) `union` f b) with ((a0 `union` f b) `union` f x). assumption.
  (* apply union_comm. *)
Admitted.

Lemma notinUnion_forAll_notin: forall mems x,
  x `notin` (fold_left (fun (ats: atoms) (m :  mem) => AtomSet.F.union ats (fv_mem m)) mems {})
 -> list_forAll (List.map (fun m : mem => x `notin` fv_mem m) mems).
Proof.
  intros. induction mems. simpl. auto. simpl in *. 
     split;
        pattern (fold_left (fun (ats : atoms) (m : mem) => ats `union` fv_mem m)
                mems ({} `union` fv_mem a)) in H;
        rewrite (foldUnionAssoc mem fv_mem mems a) in H.
          decideFSet.
          apply IHmems. decideFSet.
Qed.


(* from http://logical.futurs.inria.fr/cgi-bin/bugzilla/show_bug.cgi?id=1751#c1 *)

Definition list_f_ind (A: Set) (P : A -> Prop) (P' : list A -> Prop)
    (f:forall t, P t) (Hnil: P' nil) 
    (Hcons : forall T Ts, P T -> P' Ts -> P' (cons T Ts)) : forall l, P' l :=
 fix lf (l:list A) : P' l :=
   match l return P' l with 
   | nil => Hnil 
   | a::tl => Hcons _ _ (f a) (lf tl)
   end. 

(** Defining our own induction principle, as Coq does not consider subterms with types such as "option tp",
With the standard induction principle, we have to prove stuff about a `tp_struct optSelf mems` without 
knowing anything about optSelf and mems. With our more powerful induction principle, this case gets two
extra hypotheses:
  in case optSelf was Some t: P0 t and P1lst ms
  in case optSelf was None: P1lst ms

The user of the induction principle has to prove P1nil and P1cons below (inductively, these say that 
P1list holds for a list if P1 holds for every element of that list)

We use a section to avoid having to repeat all these variables.
*)
Section Induction.

(* variables will automatically be abstracted over where needed once section is closed (p. 32) *)
(* expanding the case for option tm and option tp inline, don't want to generate two more P's -- or would that be better? *)
Variables  (P : tm -> Prop) (P0 : tp -> Prop) (P1 : mem -> Prop) (P1lst : list mem -> Prop)
  (f : forall n : nat, P n)  (*case fvar*)
  (f0 : forall a : atom, P a) (*case bvar *)
  (f1 : forall t : tm, P t -> forall l : lab, P (sel t l)) (*case sel*)
  (f2 : forall t : tp, P0 t -> P (new t))  (* case new t *)
  (f3n : forall (ms : list mem),  P1lst ms -> P0 (tp_struct None  ms))  (* case tp_struct None _ *)
  (f3s : forall (t : tp) (ms : list mem),  P0 t -> P1lst ms -> P0 (tp_struct (Some t) ms)) (* case tp_struct (Some t) _*)
  (f4n : forall (l : lab) (t : tp), P0 t -> P1 (mtm l t None))  (* case mtm _ _ None *)
  (f4s : forall (l : lab) (t : tp) (rhs: tm), P0 t -> P rhs -> P1 (mtm l t (Some rhs))) (* case mtm _ _ (Some rhs) *)
  (P1nil: P1lst nil) (* to relate P1 and P1lst, case for nil *)
  (P1cons : forall T Ts, P1 T -> P1lst Ts -> P1lst (cons T Ts)). (* to relate P1 and P1lst, case for cons *)

(* mostly the same as what Coq generates using 
Scheme tm_ind_3 := Induction for tm Sort Prop
  with tp_ind_3  := Induction for tp Sort Prop
  with mem_ind_3  := Induction for mem Sort Prop.

The important difference is that the last two induction principles also 
consider option's and list's of the inductive types
*)
Fixpoint my_tm_ind_3 (t : tm) : P t :=
  match t as t0 return (P t0) with
  | bvar n => f n
  | fvar a => f0 a
  | sel t0 l => f1 t0 (my_tm_ind_3 t0) l
  | new t0 => f2 t0 (my_tp_ind3 t0)
  end
with my_tp_ind3 (t : tp) : P0 t :=
  match t as t0 return (P0 t0) with
  | tp_struct None ms => f3n ms (list_f_ind mem P1 P1lst my_mem_ind3 P1nil P1cons ms)
  | tp_struct (Some t) ms => f3s t ms (my_tp_ind3 t) (list_f_ind mem P1 P1lst my_mem_ind3 P1nil P1cons ms)
  end
with my_mem_ind3 (m : mem) : P1 m :=
  match m as m0 return (P1 m0) with
  | mtm l t None => f4n l t (my_tp_ind3 t)
  | mtm l t (Some rhs) => f4s l t rhs (my_tp_ind3 t) (my_tm_ind_3 rhs)
  end.


Lemma tm_tp_mem_mutual_ind:
       (forall tm0 : tm, P tm0) /\  (forall tp0 : tp, P0 tp0) /\ (forall mem0 : mem, P1 mem0)  /\ (forall mems : list mem, P1lst mems).
Proof.
 intros. split. apply (my_tm_ind_3); assumption.
 split. apply (my_tp_ind3); assumption.
 split. apply (my_mem_ind3); assumption.
 apply (list_f_ind mem P1 P1lst my_mem_ind3). auto. auto.
Qed.

End Induction.

Lemma subst_fresh : forall (x : atom) u,
  (forall e, x `notin` fv_tm e -> [x ~> u] e = e) /\ 
  (forall t, x `notin` fv_tp t -> [x ~tp> u] t = t) /\ 
  (forall m, x `notin` fv_mem m -> [x ~mem> u] m = m) /\ 
  (forall ms, list_forAll (List.map (fun m => x `notin` fv_mem m -> [x ~mem> u] m = m) ms)).
Proof.
  intros x u.
  apply tm_tp_mem_mutual_ind; intros; simpl.

  (*case fvar*)
    auto.
  
  (* case bvar *)
    destruct (a == x).
      subst. induction H. simpl. decideFSet. auto.

  (* case sel *)
   f_equal. apply H. apply H0.


  (* case new t *)
   f_equal. apply H. apply H0.

  (* case tp_struct *)
   (* case no self type*)
     f_equal.
     apply list_forAll_eq_dist.
     apply (list_forAll_MP mem ms _ _ H).
     simpl in H0. apply notinUnion_forAll_notin. auto.

   (* case self type *)
     f_equal. 
       (* self type *)
       f_equal. apply H. simpl in H1. auto.
       
       (* members *)
       apply list_forAll_eq_dist.
       apply (list_forAll_MP mem ms _ _ H0).
       simpl in H1. apply notinUnion_forAll_notin. auto.

   (* case mtm no rhs*)
   f_equal. apply H. simpl in H0. auto.

   (* case mtm rhs*)
   f_equal. 
     apply H. simpl in H1. auto.
     f_equal. apply H0. simpl in H1. auto.
 
   auto.
   auto.
Qed.




(*************************************************************************)
(** * Opening *)
(*************************************************************************)

(** Opening replaces an index with a term. It corresponds to informal
    substitution for a bound variable, such as in the rule for beta
    reduction. Note that only "dangling" indices (those that do not
    refer to any abstraction) can be opened. Opening has no effect for
    terms that are locally closed.

    Natural numbers are just an inductive datatype with two
    constructors: O and S, defined in Coq.Init.Datatypes.
    The notation [k === i] is the decidable equality function for
    natural numbers (cf. Coq.Peano_dec.eq_nat_dec).
    This notation is defined in the [Metatheory] library.

    We make several simplifying assumptions in defining [open_rec].

    First, we assume that the argument [u] is locally closed.  This
    assumption simplifies the implementation since we do not need to
    shift indices in [u] when passing under a binder.  Second, we
    assume that this function is initially called with index zero and
    that zero is the only unbound index in the term.  This eliminates
    the need to possibly subtract one in the case of indices.

    There is no need to worry about variable capture because bound
    variables are indices.
*)

Fixpoint open_rec_tm (k : nat) (u : tm) (e : tm) {struct e} : tm :=
  match e with
    | bvar i => if k === i then u else (bvar i)
    | fvar x => fvar x
    | sel e1 l => sel (open_rec_tm k u e1) l
    | new T => new (open_rec_tp k u T)
  end
with open_rec_tp (k : nat) (u : tm) (t : tp) {struct t} : tp :=
  match t with
    | tp_struct self mems => tp_struct (option_map (open_rec_tp k u) self) 
           (List.map (open_rec_mem (k+1)(* go under binder (the self variable) *) u) mems)
  end
with open_rec_mem (k : nat) (u : tm) (m : mem) {struct m} : mem :=
  match m with
    | mtm l T rhs => mtm l (open_rec_tp k u T)  (option_map (open_rec_tm k u) rhs)
  end.

(** We also define a notation for [open_rec].
*)

Notation "{ k ~> u } t" := (open_rec_tm k u t) (at level 67).
Notation "{ k ~tp> u } t" := (open_rec_tp k u t) (at level 67).
Notation "{ k ~mem> u } m" := (open_rec_mem k u m) (at level 67).

(** Many common applications of opening replace index zero with an
    expression or variable.  The following definition provides a
    convenient shorthand for such uses.  Note that the order of
    arguments is switched relative to the definition above.  For
    example, [(open e x)] can be read as "substitute the variable [x]
    for index [0] in [e]" and "open [e] with the variable [x]."
    Recall that the coercions above let us write [x] in place of
    [(fvar x)].
*)

Definition open e u := open_rec_tm 0 u e.
Definition open_tp e u := open_rec_tp 0 u e.
Definition open_mem e u := open_rec_mem 0 u e.



(*************************************************************************)
(** * Local closure *)
(*************************************************************************)

(** Recall that [tm, tp, mem] admit terms that contain unbound indices. 
    We say that a term is locally closed, 
    when no indices appearing in it are unbound.  The proposition 
    [lc e] holds when an expression [e] is locally closed.

    The inductive definition below formalizes local closure such that
    the resulting induction principle serves as the structural
    induction principle over (locally closed) expressions.  In
    particular, unlike induction for type exp, there is no case
    for bound variables.  Thus, the induction principle corresponds more
    closely to informal practice than the one arising from the
    definition of pre-terms.
*)

Inductive  lc_tp : tp -> Prop :=
  | lc_struct_noself : forall L mems,
      (forall x:atom, x `notin` L -> lc_mems (List.map (open_rec_mem 0 x) mems)) ->
      lc_tp (tp_struct None mems)
  | lc_struct_self : forall L self mems,
      lc_tp self ->
      (forall x:atom, x `notin` L -> lc_mems (List.map (open_rec_mem 0 x) mems)) ->
      lc_tp (tp_struct (Some self) mems)
with lc_mem : mem -> Prop :=
  | lc_mtm_norhs : forall l t,
      lc_tp t ->
      lc_mem (mtm l t None)
  | lc_mtm_rhs : forall l t rhs,
      lc_tp t ->
      lc_tm rhs ->
      lc_mem (mtm l t (Some rhs))
with lc_tm : tm -> Prop :=
  | lc_var : forall x,
      lc_tm (fvar x)
  | lc_sel : forall tgt l,
      lc_tm tgt ->
      lc_tm (sel tgt l)
  | lc_new : forall t,
      lc_tp t ->
      lc_tm (new t)
with lc_mems : list mem -> Prop :=
  | lc_nil :
      lc_mems (nil)
  | lc_cons : forall m ms,
      lc_mem m -> lc_mems ms -> lc_mems (m :: ms).
(*
Inductive  lc_tp : tp -> Prop :=
  | lc_struct : forall L self mems,
      option_forAll (option_map lc_tp self) ->
      (forall x:atom, x `notin` L -> list_forAll (List.map (fun m => lc_mem (open_rec_mem 0 x m)) mems)) ->
      lc_tp (tp_struct self mems)
with lc_mem : mem -> Prop :=
  | lc_mtm : forall l t rhs,
      lc_tp t ->
      option_forAll (option_map lc_tm rhs) ->
      lc_mem (mtm l t rhs)
with lc_tm : tm -> Prop :=
  | lc_var : forall x,
      lc_tm (fvar x)
  | lc_sel : forall tgt l,
      lc_tm tgt ->
      lc_tm (sel tgt l)
  | lc_new : forall t,
      lc_tp t ->
      lc_tm (new t).
*)

Hint Constructors lc_tp lc_mem lc_tp lc_mems.


(** At this point we are still stuck because the IH concerns
   [open e x] instead of [e]. The result that
   we need is that if an index substitution has no effect for
   an opened term, then it has no effect for the raw term (as long
   as we are *not* substituting for 0, hence S k below).
<<
   open e x = {S k ~> u}(open e x)  -> e = {S k ~> u} e
>>
   In other words, expanding the definition of open:
<<
   {0 ~> x}e = {S k ~> u}({0 ~> x} e)  -> e = {S k ~> u} e
>>
   Of course, to prove this result, we must generalize
   0 and S k to be any pair of inequal numbers to get a strong
   enough induction hypothesis for the abs case.
 *)



Lemma open_rec_lc_core : 
  (forall e j v i u, i <> j ->  {j ~> v} e = {i ~> u} ({j ~> v} e) -> {i ~> u} e = e) /\ 
  (forall t j v i u, i <> j ->   {j ~tp> v} t = {i ~tp> u} ({j ~tp> v} t) -> {i ~tp> u} t = t) /\ 
  (forall m j v i u, i <> j ->   {j ~mem> v} m = {i ~mem> u} ({j ~mem> v} m) -> {i ~mem> u} m = m) /\ 
  (forall ms j v i u, i <> j ->  list_forAll (List.map (fun m => {j ~mem> v} m = {i ~mem> u} ({j ~mem> v} m) -> {i ~mem> u} m = m) ms)).
Proof.
  apply tm_tp_mem_mutual_ind;  simpl in *.  
(*  induction e; intros j v i u Neq H; simpl in *.*)

  (*case bvar*)
      intros n j v i u Neq H. destruct (j === n);  destruct (i === n).
      Case "j = n = i".
        subst n. intros. destruct Neq. auto.
      Case "j = n, i <> n".
        auto.
      Case "j <> n, i = n".
        subst n. simpl in H. destruct (i === i). auto. destruct n. auto.
      Case "j <> n, i <> n".
        auto.
 
   (* case fvar *)
     auto.

   (* case sel *) 
     intros. f_equal. inversion H1. eapply H. apply H0. apply H3.

   (* case new *) 
     intros. f_equal. inversion H1. eapply H. apply H0. apply H3.

   (* case tp_struct *)
     intros. f_equal. inversion H1. apply list_forAll_eq_dist. Check list_forAll_MP. 
     apply list_forAll_MP with (P := (fun m : mem =>
        {j + 1 ~mem> v}m = {i + 1 ~mem> u}({j + 1 ~mem> v}m))). eapply H with (i := i + 1) (u := u) (j := j + 1) (v := v).
     omega.

     (* proving the P introduced by list_forAll_MP *)
     rewrite list_map_compose in H3. apply list_forAll_eq_dist2_conv. assumption. 

    intros.  f_equal. f_equal. eapply H. apply H1. inversion H2. apply H4.
      inversion H2. apply list_forAll_eq_dist. 
      apply list_forAll_MP with (P := (fun m : mem =>
        {j + 1 ~mem> v}m = {i + 1 ~mem> u}({j + 1 ~mem> v}m))). 
      eapply H0 with (i := i + 1) (u := u) (j := j + 1) (v := v).
     omega.

     rewrite list_map_compose in H5. apply list_forAll_eq_dist2_conv. assumption. 

   (* case mtm *)
     intros. f_equal. inversion H1. eapply H. apply H0. apply H3.

     intros. f_equal. inversion H2. eapply H. apply H1. apply H4.
     f_equal. inversion H2. eapply H0. apply H1. apply H5.

    auto.

    intros. split. apply H. apply H1. apply H0. apply H1.
Qed.


Section Induction_lc.

Variables (P : forall t : tm, lc_tm t -> Prop)
  (P0 : forall t : tp, lc_tp t -> Prop)
  (P1 : forall m : mem, lc_mem m -> Prop)
  (P2 : forall l : list mem, lc_mems l -> Prop)
  (f : forall x : atom, P x (lc_var x))
  (f0 : forall (tgt : tm) (l : lab) (l0 : lc_tm tgt),
        P tgt l0 -> P (sel tgt l) (lc_sel tgt l l0))
  (f1 : forall (t : tp) (l : lc_tp t), P0 t l -> P (new t) (lc_new t l))
  (f2 : forall (L : atoms) (mems : list mem)
          (l : forall x : atom,
               x `notin` L -> lc_mems (List.map (open_rec_mem 0 x) mems)),
        (forall (x : atom) (n : x `notin` L),
         P2 (List.map (open_rec_mem 0 x) mems) (l x n)) ->
        P0 (tp_struct None mems) (lc_struct_noself L mems l))
  (f3 : forall (L : atoms) (self : tp) (mems : list mem) (l : lc_tp self),
        P0 self l ->
        forall
          l0 : forall x : atom,
               x `notin` L -> lc_mems (List.map (open_rec_mem 0 x) mems),
        (forall (x : atom) (n : x `notin` L),
         P2 (List.map (open_rec_mem 0 x) mems) (l0 x n)) ->
        P0 (tp_struct (Some self) mems) (lc_struct_self L self mems l l0))
  (f4 : forall (l : lab) (t : tp) (l0 : lc_tp t),
        P0 t l0 -> P1 (mtm l t None) (lc_mtm_norhs l t l0))
  (f5 : forall (l : lab) (t : tp) (rhs : tm) (l0 : lc_tp t),
        P0 t l0 ->
        forall l1 : lc_tm rhs,
        P rhs l1 -> P1 (mtm l t (Some rhs)) (lc_mtm_rhs l t rhs l0 l1))
  (f6 : P2 nil lc_nil)
  (f7 : forall (m : mem) (ms : list mem) (l : lc_mem m),
        P1 m l ->
        forall l0 : lc_mems ms, P2 ms l0 -> P2 (m :: ms) (lc_cons m ms l l0)).

Scheme lc_tm_ind_4 := Induction for lc_tm Sort Prop
  with lc_tp_ind_4  := Induction for lc_tp Sort Prop
  with lc_mem_ind_4  := Induction for lc_mem Sort Prop
  with lc_mems_ind_4  := Induction for lc_mems Sort Prop.
Check lc_tp_ind_4.
Check lc_tm_ind_4.
Print lc_tm_ind_4.


Lemma lc_tm_tp_mem_mems_mutual_ind: 
  (forall (t : tm) (l : lc_tm t), P t l)     /\
  (forall (t : tp) (l : lc_tp t), P0 t l)    /\
  (forall (t : mem) (l : lc_mem t), P1 t l)  /\
  (forall (ms : list mem), list_forAll (List.map (fun m => forall l : lc_mem m, P1 m l) ms)).
(*  (forall (t : list mem) (l : lc_mems t), P2 t l).*)
Proof.
   intros. split. 
     apply (lc_tm_ind_4 P P0 P1 P2 f f0 f1 f2 f3 f4 f5 f6 f7); assumption.
   split. 
     apply (lc_tp_ind_4 P P0 P1 P2 f f0 f1 f2 f3 f4 f5 f6 f7); assumption.
   split. 
     apply (lc_mem_ind_4 P P0 P1 P2 f f0 f1 f2 f3 f4 f5 f6 f7); assumption.
  
   intros. 
   induction ms; simpl in *.
     auto. 
     split.
       apply (lc_mem_ind_4 P P0 P1 P2 f f0 f1 f2 f3 f4 f5 f6 f7); assumption.
       assumption.
(*   apply (lc_mems_ind_4 P P0 P1 P2 f f0 f1 f2 f3 f4 f5 f6 f7); assumption.*)
Qed.

End Induction_lc.




(* because of the mutual induction, can't use generalize dependent -- distribute the forall k over the conjunction manually *)
Lemma open_rec_lc : forall u,
  (forall e, lc_tm e -> forall k, {k ~> u} e = e) /\
  (forall e, lc_tp e -> forall k, {k ~tp> u} e = e) /\
  (forall e, lc_mem e ->  forall k, {k ~mem> u} e = e) /\
  (forall ms, list_forAll (List.map (fun m => lc_mem m ->  forall k, {k ~mem> u} m = m) ms)).

Proof.
  intros u.
  apply lc_tm_tp_mem_mems_mutual_ind with 
     (P1 := (fun m => fun _ : lc_mem m =>  forall k, {k ~mem> u} m = m))
     (P2 := (fun ms => fun _ : lc_mems ms => list_forAll (List.map (fun m => forall l : lc_mem m, forall k, {k ~mem> u} m = m) ms))).
(*(P := (fun e => fun _ : lc_tm e =>  forall k, {k ~> u} e = e)).*)
  
  (* bvar *)  
    simpl. auto.

    intros. simpl. f_equal. apply H.
    intros. simpl. f_equal. apply H.

    intros. simpl. f_equal. 

Show Proof. (* used to factor out lemma, so we can reuse it for the case tp_struct with self type *)

Lemma tp_struct_mems:  forall (u : tm) (L : atoms) (mems : list mem),
     (forall x : atom,
      x `notin` L -> lc_mems (List.map (open_rec_mem 0 x) mems)) ->
     (forall x : atom,
      x `notin` L ->
      list_forAll
        (List.map
           (fun m : mem => lc_mem m -> forall k : nat, {k ~mem> u}m = m)
           (List.map (open_rec_mem 0 x) mems))) ->
     forall k : nat, List.map (open_rec_mem (k + 1) u) mems = mems.
Proof.
  intros.
  pick fresh x for L.

(* work towards applying list_forAll_MP:

  P -> Q := H : forall x : atom,
      x `notin` L ->
      list_forAll
        (List.map
           (fun m : mem => lc_mem (open_rec_mem 0 x m) -> forall k : nat, {k ~mem> u}(open_rec_mem 0 x m) = (open_rec_mem 0 x m))
            mems)
  P := l : forall x : atom,
      x `notin` L -> list_forAll (List.map (fun m: mem => lc_mem (open_rec_mem 0 x m)) mems)

--> we want to prove this:
  Q : forall x : atom,
      x `notin` L ->
      list_forAll
        (List.map
           (fun m : mem => forall k : nat, {k ~mem> u}(open_rec_mem 0 x m) = (open_rec_mem 0 x m))
            mems)

first, massage l into a suitable shape:
 *)
  assert (forall x : atom,
      x `notin` L -> list_forAll (List.map (fun m: mem => lc_mem (open_rec_mem 0 x m)) mems)).
  intros.
  induction mems; simpl in *; auto.
    split.
      (* TODO: is there a directer way to do `inversion (H x Fr)` ? *) 
      assert (lc_mems (({0 ~mem> x0}a) :: List.map (open_rec_mem 0 x0) mems)). apply H. assumption. inversion H2.
        assumption.
      apply IHmems.
        intros. 
        assert (lc_mems (({0 ~mem> x1}a) :: List.map (open_rec_mem 0 x1) mems)). apply H. assumption. inversion H3. 
          assumption.
            intros. destruct (H0 x1 H2). assumption.
   
(* now, somehow merge the two maps in H into one using list_map_compose2*)   
   assert (forall x : atom,
      x `notin` L ->
      list_forAll
        (List.map
           (fun m : mem => lc_mem (open_rec_mem 0 x m) -> forall k : nat, {k ~mem> u}(open_rec_mem 0 x m)  = (open_rec_mem 0 x m)) mems)).
   intros.
     Check list_map_compose2.
     replace (List.map (fun m : mem => lc_mem ({0 ~mem> x0}m) -> forall k0 : nat, {k0 ~mem> u}({0 ~mem> x0}m) = {0 ~mem> x0}m) mems) 
       with  (List.map (fun m : mem => lc_mem m -> forall k : nat, {k ~mem> u}m = m) (List.map (open_rec_mem 0 x0) mems)).
       apply H0.
       assumption.
     Check list_map_compose2.
       apply (list_map_compose2 _ _ _ mems (fun m : mem => lc_mem m -> forall k : nat, {k ~mem> u}m = m) (open_rec_mem 0 x0)).

   assert ( list_forAll
         (List.map
            (fun m : mem =>
             forall k : nat, {k ~mem> u}({0 ~mem> x}m) = {0 ~mem> x}m) mems)).
Check list_forAll_MP.
    apply (list_forAll_MP _ mems (fun m : mem => lc_mem ({0 ~mem> x}m)) (fun m : mem => forall k0 : nat, {k0 ~mem> u}({0 ~mem> x}m) = {0 ~mem> x}m)).
      apply (H2 x Fr).
      apply (H1 x Fr).

Check list_forAll_eq_dist.
   rewrite -> (list_forAll_eq_dist _ mems (open_rec_mem (k + 1) u)). auto.
 

   apply under_forAll_map with (f := (fun m : mem =>
             forall k : nat, {k ~mem> u}({0 ~mem> x}m) = {0 ~mem> x}m)) (g := (fun x0 : mem => {k + 1 ~mem> u}x0 = x0)).
   intros.
   destruct open_rec_lc_core as [ _ [_ [Hmem _]]].
   apply (Hmem x0 0 x (k + 1) u).
     omega.
     symmetry.
     apply (H4 (k+1)).
   assumption.
Qed.

   (* finish case tp_struct without self type: *)
   apply (tp_struct_mems u L mems l H k).

   (* tp_struct with self type *)
   intros. simpl. f_equal. 
     f_equal. apply H.
     apply (tp_struct_mems u L mems l0 H0 k).

   intros. simpl. f_equal. apply H.
   intros. simpl. f_equal. apply H.
     f_equal. apply H0.
   intros. simpl. f_equal. auto.
   intros. simpl. f_equal. auto.   
Qed.


Lemma subst_open_rec : forall e1 e2 x,
  lc_tm e1 -> 
  (forall u k, [x ~> e1] ({k ~> e2} u) = {k ~> [x ~> e1] e2} ([x ~> e1] u)) /\
  (forall u k, [x ~tp> e1] ({k ~tp> e2} u) = {k ~tp> [x ~> e1] e2} ([x ~tp> e1] u)) /\
  (forall u k, [x ~mem> e1] ({k ~mem> e2} u) = {k ~mem> [x ~> e1] e2} ([x ~mem> e1] u)) /\
  (forall ms k, list_forAll (List.map (fun u => [x ~mem> e1] ({k ~mem> e2} u) = {k ~mem> [x ~> e1] e2} ([x ~mem> e1] u)) ms)).
Proof.
  intros e1 e2 x Hlc.
  apply tm_tp_mem_mutual_ind;  simpl in *.  
 
  intros n k. destruct (k === n).  
    auto. 
    simpl in *. auto.

  intros a k.
    Check open_rec_lc.
     destruct (open_rec_lc ([x ~> e1]e2)) as [Htm _]. 
     destruct (a == x).
       symmetry. 
         apply Htm. assumption. 
       auto. 

   intros. f_equal. apply H.
   intros. f_equal. apply H.
   intros. f_equal. 
     rewrite -> (list_map_compose2 _ _ _ ms (subst_mem x e1) (open_rec_mem (k + 1) e2)).
     rewrite -> (list_map_compose2 _ _ _ ms (open_rec_mem (k + 1) ([x ~> e1]e2)) (subst_mem x e1)).
     rewrite -> (list_forAll_eq_dist2 _ ms (fun x0 : mem => [x ~mem> e1]{k + 1 ~mem> e2}x0) (fun x0 : mem => {k + 1 ~mem> [x ~> e1]e2}([x ~mem> e1]x0))). auto.
       apply H.

   intros. f_equal. 
     f_equal. apply H.
     rewrite -> (list_map_compose2 _ _ _ ms (subst_mem x e1) (open_rec_mem (k + 1) e2)).
     rewrite -> (list_map_compose2 _ _ _ ms (open_rec_mem (k + 1) ([x ~> e1]e2)) (subst_mem x e1)).
     rewrite -> (list_forAll_eq_dist2 _ ms (fun x0 : mem => [x ~mem> e1]{k + 1 ~mem> e2}x0) (fun x0 : mem => {k + 1 ~mem> [x ~> e1]e2}([x ~mem> e1]x0))). auto.
       apply H0.

   intros. f_equal. apply H.
   intros. f_equal. apply H.
     f_equal. apply H0.

   auto.

   auto.
Qed.


Lemma subst_open_var : forall e1 (x y: atom),
  y <> x ->
  lc_tm e1 -> 
  (forall u, open ([x ~> e1] u) y = [x ~> e1] (open u y)) /\
  (forall u, open_tp ([x ~tp> e1] u) y = [x ~tp> e1] (open_tp u y)) /\
  (forall u, open_mem ([x ~mem> e1] u) y = [x ~mem> e1] (open_mem u y)) /\
  (forall ms, list_forAll (List.map (fun u => open_mem ([x ~mem> e1] u) y = [x ~mem> e1] (open_mem u y)) ms)).
Proof.
  intros e1 x y HNeq Hlc.   
  unfold open. unfold open_tp. unfold open_mem.
Check subst_open_rec.

  split. destruct (subst_open_rec e1 y x Hlc) as [H [_ [_ _]]].
  intros. symmetry. simpl in H.  
    destruct (y==x). 
      simpl. subst y.  destruct HNeq.  auto. 
      apply (H u 0).

  split. destruct (subst_open_rec e1 y x Hlc) as [_ [H [_ _]]].
  intros. symmetry. simpl in H.  
    destruct (y==x). 
      simpl. subst y.  destruct HNeq.  auto. 
      apply (H u 0).

  split. destruct (subst_open_rec e1 y x Hlc) as [_ [_ [H _]]].
  intros. symmetry. simpl in H.  
    destruct (y==x). 
      simpl. subst y.  destruct HNeq.  auto. 
      apply (H u 0).

  destruct (subst_open_rec e1 y x Hlc) as [_ [_ [_ H]]].
  intros ms.
  Check under_forAll_map.  
  apply (under_forAll_map _ ms (fun u : mem =>
            [x ~mem> e1]{0 ~mem> y}u = {0 ~mem> [x ~> e1]y}([x ~mem> e1]u)) (fun u : mem => {0 ~mem> y}([x ~mem> e1]u) = [x ~mem> e1]{0 ~mem> y}u)).
    intros. symmetry. simpl in H0.
      destruct (y==x). 
        simpl. subst y.  destruct HNeq.  auto. 
        assumption.
    auto.
Qed.


Lemma lc_mems_forAll: forall ms, lc_mems ms -> list_forAll (List.map lc_mem ms).
Proof.
  intros.
  induction ms.
    simpl. auto. 
    simpl in *. inversion H. 
      split. 
        assumption.
        apply IHms. assumption.
Qed.

Lemma lc_mems_forAll_conv: forall ms, list_forAll (List.map lc_mem ms) -> lc_mems ms.
Proof.
  intros.
  induction ms.
    auto. 
    simpl in *. inversion H.   apply lc_cons.
        assumption.
        apply IHms. assumption.
Qed.

Lemma subst_lc : forall (x : atom) u,
  lc_tm u ->
  (forall e,  lc_tm e -> lc_tm ([x ~> u] e)) /\
  (forall e,  lc_tp e -> lc_tp ([x ~tp> u] e)) /\
  (forall e,  lc_mem e -> lc_mem ([x ~mem> u] e)) /\
  (forall ms, list_forAll (List.map (fun e => lc_mem e -> lc_mem ([x ~mem> u] e)) ms)).
Proof. 
  intros x u Hu.
  apply lc_tm_tp_mem_mems_mutual_ind with 
     (P1 := (fun m => fun _ : lc_mem m =>  lc_mem ([x ~mem> u] m)))
     (P2 := (fun ms => fun _ : lc_mems ms => list_forAll (List.map (fun m => forall l : lc_mem m, lc_mem ([x ~mem> u] m)) ms))).

  intros. simpl. destruct (x0 == x). assumption. apply lc_var. (* TODO: why does auto not invoke lc_var ? *)

  intros. simpl. apply lc_sel. assumption.

  intros. simpl. apply lc_new. assumption.

  intros. simpl. Print lc_tp. apply lc_struct_noself with (L := L `union` singleton x).
Show Proof.
Lemma subst_lc_tp_struct: forall (x : atom) (u : tm),
     lc_tm u ->
     forall (L : atoms) (mems : list mem),
     (forall x0 : atom,
      x0 `notin` L -> lc_mems (List.map (open_rec_mem 0 x0) mems)) ->
     (forall x0 : atom,
      x0 `notin` L ->
      list_forAll
        (List.map (fun m : mem => lc_mem m -> lc_mem ([x ~mem> u]m))
           (List.map (open_rec_mem 0 x0) mems))) ->
     forall x0 : atom,
     x0 `notin` (L `union` singleton x) ->
     lc_mems (List.map (open_rec_mem 0 x0) (List.map (subst_mem x u) mems)).

    intros x u Hu L mems l H x0 Fr. 
      assert (lc_mems (List.map (subst_mem x u) (List.map (open_rec_mem 0 x0) mems))).
      apply lc_mems_forAll_conv.
      rewrite (list_map_compose2 _ _ _  (List.map (open_rec_mem 0 x0) mems) lc_mem (subst_mem x u)).

      assert (forall x : atom, x `notin` L -> list_forAll (List.map lc_mem (List.map (open_rec_mem 0 x) mems))).
      intros. apply lc_mems_forAll. apply l. assumption.

      apply (list_forAll_MP _ (List.map (open_rec_mem 0 x0) mems) lc_mem  (fun m : mem => lc_mem ([x ~mem> u]m))).
        apply H. auto.
        apply H0. auto.

      apply lc_mems_forAll_conv.
      assert (list_forAll (List.map lc_mem (List.map (subst_mem x u) (List.map (open_rec_mem 0 x0) mems)))).
        apply lc_mems_forAll. assumption.
       
      replace (List.map (open_rec_mem 0 x0) (List.map (subst_mem x u) mems)) with
              (List.map (subst_mem x u) (List.map (open_rec_mem 0 x0) mems)). assumption.
     
      rewrite list_map_compose2.
      rewrite list_map_compose2.

SearchPattern (List.map _ _ = List.map _ _).

      apply map_ext.
      destruct (subst_open_var u x x0) as [_ [_ [Hmem _]]]. auto. assumption.
      intros. symmetry. unfold open_mem in Hmem. apply Hmem. 
Qed.

   apply (subst_lc_tp_struct x u Hu L mems l H).

   intros. simpl.  apply lc_struct_self with (L := L `union` singleton x). 
     assumption. 
     apply (subst_lc_tp_struct x u Hu L mems l0 H0).

   intros. simpl. apply lc_mtm_norhs. assumption.
   intros. simpl. apply lc_mtm_rhs. assumption. assumption.
   simpl. auto.
   intros. simpl. auto.
Qed.

